/* 
 * $Id: RestrictionNode.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.node;

import java.util.TreeSet;
import java.util.Stack;
import java.util.ArrayList;
import java.util.Iterator;

import org.objectweb.fractal.bpc.checker.DFSR.CheckingException;
import org.objectweb.fractal.bpc.checker.state.*;
import org.objectweb.fractal.bpc.checker.utils.AnotatedProtocol;

/**
 * This class represents the Restriction operator
 */
public class RestrictionNode extends TreeNode {

    /** Creates a new instance of RestrictionNode */
    public RestrictionNode(TreeNode node, TreeSet restriction,
            ActionRepository repository) {
        super("(" + node.protocol + ")\\\\{" + getRestr(restriction, repository) + "}");
        this.restriction = restriction;

        this.nodes = new TreeNode[1];
        this.nodes[0] = node;

    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getInitial()
     */
    public org.objectweb.fractal.bpc.checker.state.State getInitial() {
        return nodes[0].getInitial();
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#isAccepting(org.objectweb.fractal.bpc.checker.state.State)
     */
    public boolean isAccepting(
            org.objectweb.fractal.bpc.checker.state.State state) {
        if (nodes[0].isAccepting(state))
            return true;
        else {
            try {
                return getAccepting(state);
            } catch (InvalidParameterException e) {
                System.out.println("!!!! Exception while processing RestrictionNode::getAccepting() !!!!\n");
                System.exit(1);
                return false;
            }
        }
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getTransitions(org.objectweb.fractal.bpc.checker.state.State)
     */
    public TransitionPairs getTransitions(State state)
            throws InvalidParameterException, CheckingException {

        Stack stack = new Stack();
        TreeSet processed = new TreeSet();
        ArrayList result = new ArrayList();

        stack.push(state);

        while (stack.size() > 0) {
            State actual = (State) stack.pop();

            if (!processed.contains(actual)) {
                TransitionPair[] trans = nodes[0].getTransitions(actual).transitions;

                for (int i = 0; i < trans.length; ++i) {
                    Integer evindex = new Integer(trans[i].eventIndex);
                    boolean restricted = restriction.contains(new Integer(ActionRepository.getPure(evindex.intValue())));

                    if (restricted)
                        result.add(trans[i]);
                    else
                        stack.push(trans[i].state);
                }

                processed.add(actual);
            }
        }

        TransitionPair[] result1 = new TransitionPair[result.size()];
        Iterator it = result.iterator();
        int i = 0;
        while (it.hasNext())
            result1[i++] = (TransitionPair) it.next();

        return new TransitionPairs(result1);

    }

    /**
     * Finds an accepting state among the states to be collapsed.
     * 
     * @return true if there is an accepting state amon the collapsed states,
     *         false otherwise
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#isAccepting(org.objectweb.fractal.bpc.checker.state.State)
     */
    private boolean getAccepting(State state) throws InvalidParameterException {

        Stack stack = new Stack();
        TreeSet processed = new TreeSet();

        stack.push(state);

        while (stack.size() > 0) {
            State actual = (State) stack.pop();
            TransitionPair[] trans = null;
            try {
                trans = nodes[0].getTransitions(actual).transitions;
            }
            // only consent can throw this exception
            catch (CheckingException e) {
                throw new RuntimeException("Internal error error");
            }

            for (int i = 0; i < trans.length; ++i) {
                if (!restriction.contains(new Integer(ActionRepository.getPure(trans[i].eventIndex)))) {
                    if (nodes[0].isAccepting(trans[i].state))
                        return true;
                    else if (!processed.contains(trans[i].state))
                        stack.push(trans[i].state);
                }
            }
            processed.add(actual);
        }

        return false;
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getWeight()
     */
    public long getWeight() {
        if (weight != -1)
            return weight;
        else {
            return weight = nodes[0].getWeight();
        }
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#forwardCut(java.util.TreeSet)
     */
    public TreeNode forwardCut(TreeSet livingevents) {
        TreeSet exlivev = new TreeSet();

        Iterator it = livingevents.iterator();

        while (it.hasNext()) {
            Integer event = (Integer) it.next();
            if (restriction.contains(new Integer(ActionRepository.getPure(event.intValue()))))
                exlivev.add(event);
        }

        nodes[0] = nodes[0].forwardCut(exlivev);

        if (nodes[0] == null)
            return null;

        else
            return this;
    }

    /**
     * @return the symbolic name of the treenode denoting its type
     */
    public String[] getTypeName() {
        String[] result = { "Restriction", "\\\\" };
        return result;
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getAnotatedProtocol(org.objectweb.fractal.bpc.checker.state.State)
     */
    public AnotatedProtocol getAnotatedProtocol(State state) {
        return nodes[0].getAnotatedProtocol(state);
    }

    /**
     * Creates the human-readable list of operations
     * 
     * @param restriction
     *            the set of events indices
     * @param repository
     *            Action repository to obtain the events labels
     * @return the list of operation NOT to be restricted
     */
    private static String getRestr(TreeSet restriction,
            ActionRepository repository) {
        String result = new String();
        Iterator it = restriction.iterator();

        result = repository.getItemString(((Integer) it.next()).intValue());

        while (it.hasNext())
            result += ", " + repository.getItemString(((Integer) it.next()).intValue());

        return result;
    }

    //--------------------------------------------------------------------------

    /**
     * The set of transitions (eventIndices) that should be omitted from the
     * transition graph
     */
    final private TreeSet restriction;

}
